Skip to content

Conversation

@Lluc24
Copy link
Contributor

@Lluc24 Lluc24 commented Dec 4, 2025

Closes #22587: Implement Divergence Checking for Match Types

Note to Reviewers: I have rebased this branch on top of PR #24743 to resolve CI failures caused by the typeSize bug. As a result, the commit from that PR currently appears in this branch's history. Once PR #24743 is accepted and merged into main, that extra commit will automatically be skipped or dropped from this PR during the final merge process.

This pull request closes #22587 by implementing a robust divergence checking mechanism for Match Types. Currently, the compiler relies on catching StackOverflowError to handle infinite recursion during match type reduction, which is an unsafe and inefficient approach. This PR replaces that behavior by adapting the "Open Implicits" divergence checking algorithm (from SIP-31) specifically for AppliedTypes and MatchTypes.

To achieve this, I have introduced a new Property in the Context to track the history of types currently being reduced. The algorithm enforces termination by verifying that the size of the match type arguments decreases according to a lexicographical ordering. In cases where the size remains constant across a reduction step, the algorithm utilizes the history memory to verify that the Match Type arguments have not been encountered before (detecting cycles).

  1. Allowed: Decreasing Size Recursive types are permitted if the argument size strictly decreases.
type Unwrap[X] = X match
  case Option[t] => Unwrap[t]
  case _ => X

In this example, reducing Unwrap[Option[Option[Int]]] is allowed because the argument shrinks from Option[Option[Int]] to Option[Int].

  1. Allowed: Same Size (Non-Cyclic) State machines or traversals are permitted if the size remains constant, provided the exact state is not repeated.
type Increase[X, Y, Z] = (X, Y, Z) match
  case (X, Y, 0) => Increase[X, Y, 1]
  case (X, 0, _) => Increase[X, 1, 0]
  case (0, _, _) => Increase[1, 0, 0]
  case _ => "done"

Here, Increase[0,0,0] passes through all binary combinations. The algorithm permits this because, although the type size remains constant, no specific tuple combination is repeated in the history.

  1. Disallowed: Increasing Size or Cycles The algorithm correctly rejects divergence caused by growing types:
// Rejected: Argument grows (Int -> List[Int])
type Wrap[X] = X match
  case AnyVal => Wrap[List[X]]
  case AnyRef => Wrap[List[X]]

And rejects divergence caused by loops (same size, same state):

// Rejected: Cyclic reference detected (Int -> ... -> Int)
type Loop[X] = X match
  case Int => Loop[Float]
  case Float => Loop[Double]
  case Double => Loop[String]
  case String => Loop[Int]
  case _ => String

@mbovel mbovel self-requested a review December 4, 2025 10:43
case AnyVal => Wrap[List[Int]]

@main def test03(): Unit =
val e1: Wrap[Int] = ??? // error
Copy link
Member

@bishabosha bishabosha Dec 4, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

List[Int] is not AnyVal , so then it stops there right?

Copy link
Contributor Author

@Lluc24 Lluc24 Dec 6, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You're absolutely right. I've fixed the test case.

The divergence check currently applies even to match types that do not strictly reduce (stuck matches). Instead of simply stopping and returning NoType (or the stuck type), the algorithm detects the increasing size of the scrutinee and correctly returns an ErrorType.

Thanks for the catch! I would have missed that otherwise.

@Lluc24 Lluc24 force-pushed the i22587-divergence-check-MT branch from 7de6009 to 3423338 Compare December 6, 2025 12:42
@mbovel
Copy link
Member

mbovel commented Dec 11, 2025

Some failures might be due to #24730.

@mbovel
Copy link
Member

mbovel commented Dec 11, 2025

25 failings tests:

    tests/bench/tuple.scala failed
    tests/neg-deep-subtype/i17435.scala failed
    tests/neg/i12049.scala failed
    tests/neg/i15158.scala failed
    tests/neg/mt-deskolemize-2.scala failed
    tests/neg/mt-recur.cov.scala failed
    tests/neg/mt-recur.scala failed
    tests/pos-deep-subtype/tuples2.scala failed
    tests/pos/12093.scala failed
    tests/pos/13633.scala failed
    tests/pos/16583.scala failed
    tests/pos/7512.scala failed
    tests/pos/9890.scala failed
    tests/pos/i15926.extract.scala failed
    tests/pos/i15926.min.scala failed
    tests/pos/i15926.scala failed
    tests/pos/i17186b.scala failed
    tests/pos/i18175.scala failed
    tests/pos/matchtype.scala failed
    tests/pos/precise-indexof.scala failed
    tests/run-macros/annot-add-global-object failed
    tests/run/Providers.scala failed
    tests/run/i17115.scala failed
    tests/run/named-tuples-strawman-2.scala failed
    tests/warn/i13433c failed

They seem mostly related to tuples.

@Lluc24 Lluc24 force-pushed the i22587-divergence-check-MT branch from 5f55a9a to 98b1d4e Compare December 13, 2025 12:38
Previously, `typeSize` reported different values for standard `TupleN`
types (e.g., `(A, B)`) compared to their equivalent recursive pair
encodings (e.g., `A *: B *: EmptyTuple`). This discrepancy occurred
because `TupleN` is a flat `AppliedType`, while the nested encoding
forms a deeper tree structure.

This patch modifies `TypeSizeAccumulator` to canonicalize `TupleN`
types into their recursive `*:` representation before calculating
the size. This ensures that the size metric is consistent regardless
of whether the tuple is represented syntactically or structurally.

This change is verified by a new unit test in `TypesTest`, which
confirms that both `Tuple3[Int, Boolean, Double]` and its recursive
equivalent `Int *: Boolean *: Double *: EmptyTuple` now yield
identical `typeSize` values.

Fixes scala#24730
This is the first step towards implementing the full divergence check
algorithm for Match Types. The logic enforces that recursive reduction
steps must have a strictly smaller size than the sum of the type sizes
of the scrutinee.

This check applies to match types during reduction as well as those
that do not reduce. When the algorithm detects a non-decreasing size,
it returns an ErrorType to prevent infinite recursion.

This work is part of the research project specified by Martin Odersky
in issue scala#22587.
This commit relaxes the previous strict size-decreasing constraint for
Match Type reduction, allowing for more expressive recursive types while
maintaining termination guarantees.

Key changes:
1. Lexicographical Comparison: Instead of comparing the sum of argument
   sizes, the algorithm now compares the list of argument sizes
   lexicographically. This provides a more precise metric for progress.

2. Bounded Variation: Reductions are no longer required to strictly
   decrease in size at every step. Same-size reductions are now allowed,
   provided the sequence of arguments has not been seen before in the
   current reduction chain (cycle detection).

3. History Stack: A stack of previously seen argument lists is maintained
   for the current size baseline.
   - If size strictly decreases: The stack is cleared (progress made).
   - If size increases: An ErrorType is returned (divergence).
   - If size is equal: The arguments are checked against the stack.
     Repeating arguments trigger a cycle error; new arguments are added
     to the stack.

Since the number of type combinations is finite, disallowing growth
while preventing cycles guarantees the algorithm will eventually terminate.
@Lluc24 Lluc24 force-pushed the i22587-divergence-check-MT branch from 98b1d4e to 05a86ae Compare December 13, 2025 14:16
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Implement Divergence Checking for Match Types

3 participants